Solving Real-World Problems with Logic:

A Hands-On Guide to

Satisfiability Modulo Theories and Optimization Modulo Theories

Tutorial Overview

This hands-on tutorial will teach attendees how to easily translate real-world problems into SMT/OMT formulations, making these powerful solvers accessible without requiring deep theoretical knowledge! Don’t worry if your face looks like Pikachu's right now—that’s a perfectly normal reaction to realizing how much can be solved with just a few lines of logic.

Write to gs81 [at] rice [dot] edu for more info!

About the tutorial

Many complex decision-making, optimization, and verification problems can be efficiently solved using logical reasoning tools known as satisfiability modulo theories (SMT) and optimization modulo theories (OMT) solvers, fearing they require extensive theoretical knowledge.

This tutorial bridges that gap with a hands-on approach, showing how real-world problems can be easily translated into SMT/OMT/OMT formulations. By focusing on practical applications rather than theory, attendees will gain concrete skills to integrate these solvers into their research. As formal methods play an increasing role in AI, security, and optimization, this tutorial offers immediate value to researchers, students, and industry professionals seeking efficient and scalable problem-solving techniques.

Goals & Target Audience

Objectives of the Tutorial

Lower the entry barrier to SAT, SMT, and OMT solvers.
Demystify solver usage and emphasize real-world applications.
Teach hands-on modeling and problem encoding.
Encourage broader adoption in AI, optimization, and verification.

Target Audience

AI researchers & engineers
Software verification & security professionals
Operations researchers & logicians
PhD students & early-career scientists

Tutorial outline

1. Introduction to SAT and SMT Solving (≈ 20 minutes)

Overview of SAT, SMT, and OMT solvers and their use cases
Introduction to MathSAT, OptiMathSAT, and Z3 solvers
How to express real-world problems using SAT and SMT-LIB syntax

2. Hands-on: Basic Problem Modeling (≈ 40 minutes)

Encoding constraints using Boolean logic and arithmetic
First exercises: modeling simple constraints and solving them with SMT solvers
Demonstrating the difference between SAT, SMT, and OMT formulations

3. Automating Problem Encodings and Best Practices (≈ 30 minutes)

Techniques to automate SMT encoding and avoid common pitfalls
Best practices for solver efficiency (e.g., reducing problem size, choosing the right encoding)

4. Advanced SMT Techniques and Applications (≈ 45 minutes)

Bit-vector and arithmetic encoding (e.g., cybersecurity key-cracking example)
Logical deduction and investigations (e.g., solving a murder mystery using SMT)
Using quantifiers and uninterpreted functions in Z3
Graph-based problems (e.g., shortest path, maximum clique)

5. Optimization Modulo Theories (OMT) (≈ 40 minutes)

Introduction to OptiMathSAT and multi-objective optimization
Solving scheduling, planning, and resource allocation problems using OMT

6. Q&A and Interactive Discussion (≈ 10 minutes)

Addressing participant questions
Discussing how attendees can apply SMT/OMT solving in their own research or industry projects

Resources

Part 1 - SAT & SMT

Slides: [TBA]

Notebook: [TBA]

Part 2 - SMT & OMT

Slides: [TBA]

Notebook: [TBA]

Presenter

Giuseppe Spallitta

Postdoctoral researcher

Rice University, Houston, Texas

Giuseppe Spallitta is a Research Associate at Rice University, specializing in formal verification, SMT/OMT solving, and automated reasoning. His research focuses on model counting, model enumeration, and the practical applications of SAT and SMT solvers. He previously completed his PhD at the University of Trento and worked as a visiting scholar at Albert-Ludwig University of Freiburg, collaborating with leading experts in the field.

Giuseppe has presented his work at top conferences such as AAAI, UAI, and SAT. He has also spoken at various seminars and workshops, including Python-based data analysis tutorials for non-computer scientists. His research contributions include advancements in SMT/OMT-based weighted model integration and novel approaches to SAT enumeration.

Page updated

Report abuse